feat(#1000): ship 'synth verify' in released artifacts + non-vacuity smoke gate (RQ-58-SHIPVERIFY) - #1002
Merged
Merged
Conversation
…ategy line from a binary that cannot verify Red-first: tests/verify_banner_1000.rs (no required-features) fails on the pre-fix ordering — the incapable binary printed all four 'Translation validation:' lines including 'Strategy: Per-rule SMT verification (ASIL D path)' before bailing. Exit code was already correct (#124); now nothing verification-shaped precedes the failure. The verify half (wired into fact-spec-oracle) pins that a capable binary still prints the banner and ends in a real verdict. Also de-stales the 'via Z3' help line (measured: 0 z3 nodes under --features verify). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ity smoke gate (RQ-58-SHIPVERIFY) release.yml: all four platform builds now pass --features verify (pure-Rust ordeal since #553 — re-measured: 0 z3 nodes; the z3 differential oracle stays a separate synth-verify/z3-solver opt-in). The npm channel inherits the feature: the @pulseengine/synth wrapper downloads and checksum-verifies these same tarballs at install time. Non-vacuity gate: scripts/release_verify_smoke.sh runs against the binary EXTRACTED FROM EACH PACKAGED TARBALL (aarch64-linux under qemu-user; the x86_64 macOS tarball under Rosetta on the arm64 runner) — compiles a module, runs 'synth verify' on it, and asserts a real verdict (exit 0, verdict line, synth-verify-v1 report with >=1 verified / 0 failed). Red-first, demonstrated at authoring AND pinned in CI: the fact-spec-oracle job builds a verify-less binary and asserts the script FAILS with exactly the capability error, then re-runs it green on the verify build. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
avrabe
added a commit
that referenced
this pull request
Aug 19, 2026
…ildcard was a LIVE executed miscompile (RQ-58-WILDCARD) (#1003) * fix(#946): i64-width vstack drift — if/br_if/br_table/memory.copy/call args never left the width stack The RQ-58-WILDCARD classification pass found the live hole the lane brief predicted, and it is worse than latent: an EXECUTED cross-shape miscompile. wasm_stack_effect listed If | BrIf | BrTable as (0, 0) although each pops one i32 (condition / table index), let the `_ => (0, 0)` wildcard absorb MemoryCopy/MemoryFill (which pop 3), and its Call row (0, 1) never popped call arguments. Every one of those stale entries shifts infer_i64_locals' width stack, so an i64 local set past one of these shapes was inferred i32, given a 4-byte slot and a single-word STR/LDR — hi half silently dropped. The inference is shared with the RV32 selector (#312), so the drift was cross-backend. Executed proof (unicorn vs wasmtime, cortex-m4 --relocatable --no-optimize), all returning (0x1_0000_0005 >> 32), expected 1: br_if shape -> 32 if shape -> 32 br_table shape -> 32 memory.copy shape -> 0 All four return 1 after the fix. Fix: * wasm_stack_effect: If | BrIf | BrTable -> (1, 0); MemoryCopy | MemoryFill -> (3, 0); the trailing `_ => (0, 0)` wildcard is GONE — the match is fully enumerated over all 279 WasmOp variants (SIMD rows stated per shape), so a new variant fails to COMPILE until its stack effect is stated (#615 expand-or-loud-reject pattern). * infer_i64_locals: pops call ARGUMENTS against the real arg-count tables (func_arg_counts / type_arg_counts, one slot per value — the decoder's unit) and call_indirect's table-index operand; empty tables degrade to the pre-#946 zero-arg approximation, matching lower_call's own #195 fallback. Signature threaded through compute_local_layout, both ARM call sites, and the RV32 selector (which has no type table; call_indirect is Unsupported there, so the empty slice cannot under-pop on anything that compiles). * Approximation residuals STATED, not hidden, at the structural row: post-Br/Return/Unreachable polymorphic tracking and the Else join (an if-with-result double-counts its result) need a control-frame-aware walk — named follow-up. Gates: * tests/i64_width_vstack_946.rs — 7 shape pins red on the pre-fix behavior (verified by temporary revert), 2 controls (i64-returning call #311, i32-stays-i32) green on both. * tests/selector_stack_effect_no_wildcard_946.rs — the #615-style tripwire (same scanner set as wcet_sp_no_wildcard_946.rs): no catch-all arm may regrow, every WasmOp variant must be NAMED in the body, count pinned 279, negative controls + verified red on an injected `_ =>` in the real function. * scripts/repro/i64_width_vstack_946.wat — the four executable shapes, picked up by the wired #973 ARM corpus sweep Phase B (ran locally: 4 exports x 12 vectors compared, 0 mismatches, sweep PASS with the EXPECTED_DECLINES exact-set unchanged); i64_width_vstack_mem_946.wat carries the memory.copy/fill shapes (memory section excludes it from Phase B — Phase A compile + unit pins cover it). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * chore(#946): loud-convert the silent last-variant maps + move the wildcard ratchet 56 -> 55 Classification-driven follow-through on the RQ-58-WILDCARD lane (the fix itself is the previous commit): * 8 silent-map refinements converted to expand-or-loud-reject: the six float inner matches whose `_ =>` silently lowered as the LAST variant (F32Div/F32Ge/F64Div/F64Sqrt/F64Ge/F64Nearest — a widened outer arm would have become a silent wrong lowering) now name the final variant and panic on drift; the two access-size fallbacks that silently widened any unexpected width to a WORD load/store now panic. Byte-identical by construction (whole workspace incl. all frozen anchors green, rc=0). Deliberately count-neutral: `_ => unreachable!()` still matches the ratchet regex, and swapping it for a bare-binding arm to game the count is exactly what the tripwire scanners flag. * claims.yaml: selector_wildcard_arms_code 56 -> 55 banked (value + baseline; the wasm_stack_effect wildcard is gone), arms_total 91 -> 90, lines_code 17,897 -> 17,991 with a bound waiver (the 279-variant enumeration + call-arg threading: lines traded for exhaustiveness, the trade this release wants), lines_total 28,495 -> 28,599. The remaining 55 arms' classification is recorded at the pin. status.json regenerated via --emit-status. * Ledger re-grades: RQ-58-WILDCARD proposed -> implemented (this lane); RQ-58-SHIPVERIFY proposed -> implemented (PR #1002 merged 2026-08-19 — the ledger had drifted behind the merge). * CLAUDE.md: the pin-rationale sentence kept v0.57 numbers as if live; now dated at pin creation with the live figures delegated to the pins. Gates: cargo test --workspace rc=0, clippy -D warnings clean, fmt --check clean, claim_check 49/49. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #1000 (RQ-58-SHIPVERIFY).
synth verifyexisted in the tree and in--help, failed closed with an exemplary message — and was in no artifact any user could obtain (confirmed on 0.55.0 and 0.57.0: all four platform tarballs lacked--features verify). For a compiler whose whole argument is verified code generation, this ships the feature and gates it so it cannot silently regress to help text.1. Released binaries carry
verifyrelease.yml: all four platform builds (x86_64/aarch64Linux,x86_64/aarch64macOS) now build-p synth-cli --features verify; the stale "deliberate follow-up decision" comment is replaced with the measured basis.cargo tree -p synth-cli --features verify→ 0 z3 nodes;--features verify,synth-verify/z3-solver→ 2.verify = ["synth-verify"](pure-Rust ordeal since Adopt ordeal (pure-Rust QF_BV) in synth-verify; demote Z3 to differential oracle, then drop static-link-z3 #553/v0.27); the Z3 differential oracle remains a separate opt-in that links the system libz3 and is not enabled here.@pulseengine/synthwrapper downloads and checksum-verifies these same release tarballs at install time (npm/install.js), so it inherits the feature.cargo install synth-cliusers still choose features themselves (verifyis deliberately not made a default feature — that would change every workspace build; named residual, not silently dropped).2. The non-vacuity gate (the part that matters)
scripts/release_verify_smoke.shruns against the binary extracted from each packaged tarball (not a dev build): compiles a module with it, runssynth verifyon that module, and asserts a real verdict — exit 0, the verdict line, and asynth-verify-v1report whose summary provesverified >= 1 && failed == 0(counts, not sentence-greps). All four tarballs are executed: linux-x86_64 + both macOS natively (x86_64-darwin under Rosetta on the arm64 runner), the cross-built aarch64-linux tarball underqemu-aarch64 -L /usr/aarch64-linux-gnu.Red-first evidence (local, this branch):
And the red direction is CI-pinned, not authoring-time-only: the
fact-spec-oraclejob now builds a verify-less binary, asserts the smoke script FAILS with exactly the capability error (wrong-reason failures are also red), then re-runs it green on the verify build. A gate whose red leg is not exercised goes vacuous silently — this repo has shipped that class.3. Capability check before the banner
Previously the four
Translation validation:lines — includingStrategy: Per-rule SMT verification (ASIL D path)— printed before the tool discovered it could not verify, so a log-scraper found the ASIL-D strategy line in a run that verified nothing (exit code was already correct, #124). The check now runs before the banner: an incapable binary prints nothing verification-shaped before failing.Red-first:
tests/verify_banner_1000.rs(norequired-features; the missing-capability half runs in the plain workspace suite) fails on the pre-fix ordering — observed:ASIL-D strategy line printed by a binary that cannot verify— and passes with the fix. The#[cfg(feature = "verify")]half (wired intofact-spec-oracle) pins that a capable binary still prints the banner and ends inAll functions verified successfully..Also de-staled the
synth verifyhelp line ("via Z3" → SMT translation validation, pure-Rust ordeal) — measured above.Out of scope, named not silently dropped
#1000's
synthesize-vs-compiledescription overlap,--format json, help-line width (real, minor, not this lane's subject); makingverifya default cargo feature; README:98's stale Z3 sentence (corrected in #1001 — not duplicated here).Step 5 — witness MC/DC (#978 floors)
The reordered capability check adds one decision — in
synth-cli, which is outside the scored scope. The harness's full in-workspace closure issynth-mcdc-harness+synth-core/synth-cfg/synth-opt/synth-synthesis/synth-backend-riscv(percargo tree), andgit diff --name-only main...HEADintersects it in 0 files (Cargo.lock also unchanged, rustc pinned 1.96.1): the harness wasm this branch produces is byte-for-byte main's, so the counts cannot move.I re-derived locally anyway at rustc 1.96.1 and READ THE GAP ROWS rather than trusting the argument: every gap-row function is in the untouched crates (
validate_final_allocation_rv32,ensure_supported_target,compile_function_with_opts,static_data_addr::resolve_owner/validate_reloc_resolutions*) — none is this lane's code. Honest boundary on the local numbers: my localwitness-mcdcis 0.28.0, not the CI-pinned 0.42.0, and the local run reports 122 cond / 50 proved / 51 dead vs floors 130/57/≤50 — since the harness inputs are provably identical to main's, that local red is the unpinned local witness version measuring differently, not a delta from this change (it would reproduce identically on main). The PR'smcdc-structural-coveragejob (pinned witness 0.42.0, pinned host) is the authoritative floors gate — read its result, not my local one.Step 6 — sigil / attestation
Assessed, not defaulted to N/A: this PR changes what the released tarballs contain (a larger binary with the ordeal solver linked in). The existing attestation chain covers the new content without modification — SLSA provenance is generated per-release over
release-assets/*.tar.gz(subject digests are computed from the new bytes) and the cosign-signedSHA256SUMS.txttransitively covers them; the smoke step runs before upload/attestation and does not modify the archives. No new artifact type or build stage is introduced, and synth's native tarballs are not sigil-signed wasm (sigil is not part of this repo's release chain). Nothing to add.🤖 Generated with Claude Code
https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L